Inference at * 1 1 2 
Iof proof for Lemma list extensionality:

.....subterm..... T:t2:n

1. T : Type
2. T List
3. u : T
4. v : T List
5. b:(T List). (||v|| = ||b||)  (i:. (i < ||v||)  (v[i] = b[i]))  (v = b)
6. T List
7. u1 : T
8. v1 : T List
9. (||[u / v]|| = ||v1||)  (i:. (i < ||[u / v]||)  ([u / v][i] = v1[i]))  ([u / v] = v1)
10. ||v||+1 = ||v1||+1
11. i:. (i < (||v||+1))  ([u / v][i] = [u1 / v1][i])
  v = v1 

latex

 by ((BackThruSomeHyp) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok SupInf:t) inil_term))) 

latex

C1: 

C1: 12. i : 
C1: 13. i < ||v||
C1:   v[i] = v1[i]
C.

Definitions	, t  T, P  Q, x:A. B(x),
Lemmas	nat wf, length wf1